<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>Missing theorems from Freek Wiedijk's list of 100 theorems</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  
<h1 id="missing-theorems-from-a-hrefhttpswwwcsrunlfreekfreek-wiedijksa-a-hrefhttpswwwcsrunlfreek100list-of-100-theoremsa" class="markdown-heading">Missing theorems from <a href="https://www.cs.ru.nl/~freek/">Freek Wiedijk's</a> <a href="https://www.cs.ru.nl/~freek/100/">list of 100 theorems</a> <a class="hover-link" href="#missing-theorems-from-a-hrefhttpswwwcsrunlfreekfreek-wiedijksa-a-hrefhttpswwwcsrunlfreek100list-of-100-theoremsa">#</a></h1>
<p>These theorems are not yet formalized in Lean.</p>
<ul>
<li>
<p>5: Prime Number Theorem</p>
</li>
<li>
<p>6: Godel’s Incompleteness Theorem</p>
</li>
<li>
<p>8: The Impossibility of Trisecting the Angle and Doubling the Cube</p>
</li>
<li>
<p>9: The Area of a Circle</p>
</li>
<li>
<p>12: The Independence of the Parallel Postulate</p>
</li>
<li>
<p>13: Polyhedron Formula</p>
</li>
<li>
<p>14: Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + ….</p>
</li>
<li>
<p>15: Fundamental Theorem of Integral Calculus</p>
</li>
<li>
<p>16: Insolvability of General Higher Degree Equations</p>
</li>
<li>
<p>18: Liouville’s Theorem and the Construction of Trancendental Numbers</p>
</li>
<li>
<p>21: Green’s Theorem</p>
</li>
<li>
<p>23: Formula for Pythagorean Triples</p>
</li>
<li>
<p>26: Leibnitz’s Series for Pi</p>
</li>
<li>
<p>28: Pascal’s Hexagon Theorem</p>
</li>
<li>
<p>29: Feuerbach’s Theorem</p>
</li>
<li>
<p>30: The Ballot Problem</p>
</li>
<li>
<p>32: The Four Color Problem</p>
</li>
<li>
<p>33: Fermat’s Last Theorem</p>
</li>
<li>
<p>35: Taylor’s Theorem</p>
</li>
<li>
<p>36: Brouwer Fixed Point Theorem</p>
</li>
<li>
<p>37: The Solution of a Cubic</p>
</li>
<li>
<p>40: Minkowski’s Fundamental Theorem</p>
</li>
<li>
<p>41: Puiseux’s Theorem</p>
</li>
<li>
<p>43: The Isoperimetric Theorem</p>
</li>
<li>
<p>45: The Partition Theorem</p>
</li>
<li>
<p>46: The Solution of the General Quartic Equation</p>
</li>
<li>
<p>47: The Central Limit Theorem</p>
</li>
<li>
<p>48: Dirichlet’s Theorem</p>
</li>
<li>
<p>49: The Cayley-Hamilton Thoerem</p>
</li>
<li>
<p>50: The Number of Platonic Solids</p>
</li>
<li>
<p>53: Pi is Trancendental</p>
</li>
<li>
<p>54: Konigsberg Bridges Problem</p>
</li>
<li>
<p>55: Product of Segments of Chords</p>
</li>
<li>
<p>56: The Hermite-Lindemann Transcendence Theorem</p>
</li>
<li>
<p>57: Heron’s Formula</p>
</li>
<li>
<p>59: The Laws of Large Numbers</p>
</li>
<li>
<p>61: Theorem of Ceva</p>
</li>
<li>
<p>62: Fair Games Theorem</p>
</li>
<li>
<p>64: L’Hopital’s Rule</p>
</li>
<li>
<p>67: e is Transcendental</p>
</li>
<li>
<p>70: The Perfect Number Theorem</p>
</li>
<li>
<p>76: Fourier Series</p>
</li>
<li>
<p>77: Sum of kth powers</p>
</li>
<li>
<p>81: Divergence of the Prime Reciprocal Series</p>
</li>
<li>
<p>83: The Friendship Theorem</p>
</li>
<li>
<p>84: Morley’s Theorem</p>
</li>
<li>
<p>87: Desargues’s Theorem</p>
</li>
<li>
<p>88: Derangements Formula</p>
</li>
<li>
<p>90: Stirling’s Formula</p>
</li>
<li>
<p>92: Pick’s Theorem</p>
</li>
<li>
<p>93: The Birthday Problem</p>
</li>
<li>
<p>95: Ptolemy’s Theorem</p>
</li>
<li>
<p>97: Cramer’s Rule</p>
</li>
<li>
<p>98: Bertrand’s Postulate</p>
</li>
<li>
<p>99: Buffon Needle Problem</p>
</li>
<li>
<p>100: Descartes Rule of Signs</p>
</li>
</ul>

  </div>
</div>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>